COMMENT ⊗   VALID 00004 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.if false then begin "notes"
C00003 00003	.ss(lambda,LAMBDA CALCULUS)
C00006 00004	.if false then begin "reconstruction of Scottery"
C00007 ENDMK
C⊗;
.if false then begin "notes"
1. λ-expressions and λ-conversion
2. statement but not proof of Church-Rosser theorem
3. universality of λ-calculus via simulation of LISP using Scott
devices.
4. remarks including
	just because you can do without explicit conditional expressions
or something else doesn't mean it's practical or even theoretically
preferable  do so
	Church's inconsistent logic
	Scott's models
	lcf
	combinators
.end "notes"
.ss(lambda,LAMBDA CALCULUS)

	The lambda notation used in LISP was taken from the lambda
calculus described by Alonzo Church in his 1940 book, %2The Calculi
of Lambda Conversion%1.  This section covers some aspects of the
lambda calculus that go beyond what is used in LISP.

	Each LISP expression either evaluates to some object 
(like %2qa_x%1)
or it
represents a function (like %2λx.[qa_x_._y]%1).
[In the terminology of logic, it has a definite
type, but the word "type" is often used differently in computer science
where numbers and list structure are considered of different types.
Logicians use the word "sort" for the computer scientist's "type"].
The lambda calculus
doesn't make this distinction, and any expression can be taken as
a function.  A lambda calculus evaluator would leave many expressions
unevaluated.

	This is more general, but a system that realized it
on a computer would most likely do everything in a more complicated
and slower way for the benefit of rarely utilized generality.  We
say "most likely", because someone may invent a way of getting the
generality without paying any operational penalty.

	Lambda calculus is much simpler than LISP in its basic structure,
and its formulas are constructed as follows:

.item←0
	#. A variable is an expression.

	#. If ⊗f and ⊗e are expressions, then so is ⊗f(e). 

	#. If ⊗v is a variable and ⊗e is an expression,
then ⊗(λv.e) is an expression.
.<<should we introduce a list form of λ-expression here?>>
.if false then begin "reconstruction of Scottery"

true = λx y. x

false = λx y. y

if p then a else b = p(a)(b)

left to right evaluation, outside in or inside out?

need cons, car, cdr, atom, eq or equal

car = λx y. x

cdr = λx y. y

cons= λx y. x(y)  ???

get a particular atom by